Nuprl Definition : es-kind-index
11,40
postcript
pdf
es-kind-index(
es
;
k
;
e
)
== if es-first(
es
;
e
)
==
then 0
==
else if eq_knd(es-kind(
es
; es-pred(
es
;
e
));
k
) then 1 else 0 fi
== else
+ es-kind-index(
es
;
k
; es-pred(
es
;
e
))
==
fi
(recursive)
latex
Definitions
Y
,
x
.
A
(
x
)
,
es-first(
es
;
e
)
,
n
+
m
,
if
b
then
t
else
f
fi
,
eq_knd(
a
;
b
)
,
es-kind(
es
;
e
)
,
#$n
,
f
(
a
)
,
es-pred(
es
;
e
)
FDL editor aliases
es-kind-index
origin
x.A(x)x.A(x)